/*
 * SYmbolic Model-Based test case generation toOL for Real-Time systems (SYMBOLRT)
 * (C) Copyright 2010-2012 Federal University of Campina Grande (UFCG)
 * 
 * This file is part of SYMBOLRT.
 *
 * SYMBOLRT is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * SYMBOLRT is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with SYMBOLRT.  If not, see <http://www.gnu.org/licenses/>.
 *
 *
 * REVISION HISTORY:
 * Author                           Date           Brief Description
 * -------------------------------- -------------- ------------------------------
 * Wilkerson de Lucena Andrade      19/04/2012     Initial version
 * 
 */
package br.edu.ufcg.symbolrt.main;

import java.util.List;

import br.edu.ufcg.symbolrt.algorithms.CompositionCompletion;
import br.edu.ufcg.symbolrt.algorithms.ParallelComposition;
import br.edu.ufcg.symbolrt.algorithms.SequentialComposition;
import br.edu.ufcg.symbolrt.algorithms.SequentialCompositionShared;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.Transition;
import br.edu.ufcg.symbolrt.compiler.facade.Compiler;
import br.edu.ufcg.symbolrt.examples.TargetDesignation;
import br.edu.ufcg.symbolrt.examples.TargetTracking;
import br.edu.ufcg.symbolrt.examples.Toy5;
import br.edu.ufcg.symbolrt.examples.Toy6;
import br.edu.ufcg.symbolrt.examples.ToyI1;
import br.edu.ufcg.symbolrt.examples.ToyI2;
import br.edu.ufcg.symbolrt.examples.ToyS1;
import br.edu.ufcg.symbolrt.examples.ToyS2;
import br.edu.ufcg.symbolrt.exception.ClockGuardException;
import br.edu.ufcg.symbolrt.facade.SYMBOLRT;
import br.edu.ufcg.symbolrt.symbolicexecution.exception.IncompatibleOperationException;
import br.edu.ufcg.symbolrt.util.GraphVisualization;


/**
 * <code>Main</code> Class. <br>
 * This class contains the main for executing the SYMBOLRT tool.
 * 
 * @author Wilkerson de Lucena Andrade  ( <a href="mailto:wilkerson@computacao.ufcg.edu.br">wilkerson@computacao.ufcg.edu.br</a> )
 * 
 * @version 1.0
 * <br>
 * SYmbolic Model-Based test case generation toOL for Real-Time systems (SYMBOLRT)
 * <br>
 * (C) Copyright 2010-2012 Federal University of Campina Grande (UFCG)
 * <br>
 * <a href="https://sites.google.com/a/computacao.ufcg.edu.br/symbolrt">https://sites.google.com/a/computacao.ufcg.edu.br/symbolrt</a>
 */
public class MainToys {

	public static void main(String[] args) {
		
		/*String usageMessage = "Usage: symbolrt [OPTION] fileName specificationName testPurposeName\n\n" +
							  "By default, SYMBOLRT compiles the specified file and show test cases for the " +
							  "indicated specification and test purpose.\n\n" +
							  "Options:\n-a	show all intermediate models\n";
		
		if ((args.length != 3) && (args.length != 4)) {
			System.out.println(usageMessage);
			System.exit(0);
		}
		
		String fileName = "";
		String specName = "";
		String tpName = "";
		boolean showModels = false;
		
		if (args.length == 3) {
			fileName = args[0];
			specName = args[1];
			tpName = args[2];
		} else if (args.length == 4) {
			if (args[0].equals("-a")) {
				showModels = true;
				fileName = args[1];
				specName = args[2];
				tpName = args[3];
			} else {
				System.out.println(usageMessage);
				System.exit(0);
			}
		}
		
		/*Compiler.compile(fileName, specName);
		List<TIOSTS> testCases = SYMBOLRT.getInstance().generateTestCases(Compiler.getSpecification(specName), Compiler.getSpecification(tpName), showModels);
		SYMBOLRT.getInstance().show(testCases);*/
		
		//Inputs for parallel composition
		TIOSTS tiosts1 = ToyI1.createSPEC();
		TIOSTS tiosts2 = ToyI2.createSPEC();
		
		//Input for Composition completion
		//TIOSTS tiosts1 = Toy5.createSPEC();
		
		SequentialComposition seqComposition = SequentialComposition.getInstance();
		ParallelComposition parComposition = ParallelComposition.getInstance();
		CompositionCompletion compCompletion = CompositionCompletion.getInstance();
		TIOSTS result;
		GraphVisualization visualization = new GraphVisualization();
					
		try {
			//result = seqComposition.sequentialComposition(tiosts1, tiosts2);
			result = parComposition.parallelComposition(tiosts1, tiosts2);	
			//result = compCompletion.complete(tiosts1);
			//visualization.show(tiosts1);

			visualization.save(result);
		    //textualVisualization(result);
		//} catch (ClockGuardException e) {
			// TODO Auto-generated catch block
			//e.printStackTrace(); 
		}catch (IncompatibleOperationException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}		
	}	
	
	private static void textualVisualization(TIOSTS tiosts){
		for(Transition t: tiosts.getTransitions()){
			System.out.println(t.getSource() +" | "+t.getAllGuard()+" | "+t.getAction()+" | "+t.getAllAssignments()+" | "+ t.getDeadline()+" | "+t.getTarget());			
		}
		
	}
}
